/-
Copyright (c) 2025 Xavier Roblot. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Xavier Roblot
-/
import Mathlib.Algebra.Field.ZMod
import Mathlib.RingTheory.Ideal.Norm.AbsNorm

/-!
# Ideal of `ℤ`

We prove results about ideals of `ℤ` or ideals of extensions of `ℤ`.

In particular, for `I` an ideal of a ring `R` extending `ℤ`, we prove several results about
`absNorm (under ℤ I)` which is the smallest positive integer contained in `I`.

## Main definitions and results

* `Int.ideal_span_isMaximal_of_prime`: the ideal generated by a prime number is maximal.

* `Int.absNorm_under_eq_sInf`: the predicate that the `absNorm (under ℤ I)` is the smallest
  positive integer in `I`.

* `Int.absNorm_under_dvd_absNorm`: `absNorm (under ℤ I)` divides the norm of `I`.

-/

instance Int.ideal_span_isMaximal_of_prime (p : ℕ) [Fact (Nat.Prime p)] :
    (Ideal.span {(p : ℤ)}).IsMaximal :=
  Ideal.Quotient.maximal_of_isField _ <|
    (Int.quotientSpanNatEquivZMod p).toMulEquiv.isField _ (Field.toIsField _)

namespace Int

open Ideal

variable {R : Type*} [Ring R] {I : Ideal R}

theorem cast_mem_ideal_iff {d : ℤ} :
    (d : R) ∈ I ↔ (absNorm (under ℤ I) : ℤ) ∣ d := by
  rw [← mem_span_singleton, ideal_span_absNorm_eq_self, under_def, mem_comap, eq_intCast]

variable (I)

theorem absNorm_under_mem :
    (absNorm (under ℤ I) : R) ∈ I := by
  rw [← cast_natCast, cast_mem_ideal_iff]

theorem absNorm_under_eq_sInf :
    absNorm (under ℤ I) = sInf {d : ℕ | 0 < d ∧ (d : R) ∈ I} := by
  by_cases h : absNorm (under ℤ I) = 0
  · have : {d : ℕ | 0 < d ∧ ↑d ∈ I} = ∅ := by
      refine Set.eq_empty_of_forall_notMem ?_
      intro x ⟨hx₁, hx₂⟩
      rw [← cast_natCast, cast_mem_ideal_iff, h, natCast_dvd_natCast, Nat.zero_dvd] at hx₂
      rw [Nat.pos_iff_ne_zero] at hx₁
      exact hx₁ hx₂
    rw [h, this, Nat.sInf_empty]
  · have h₁ : absNorm (under ℤ I) ∈ {d : ℕ | 0 < d ∧ ↑d ∈ I} :=
      ⟨Nat.pos_of_ne_zero h, absNorm_under_mem I⟩
    refine le_antisymm ?_ (Nat.sInf_le h₁)
    by_contra! h₀
    have h₂ := (Nat.sInf_mem (Set.nonempty_of_mem h₁)).2
    rw [← cast_natCast, cast_mem_ideal_iff, natCast_dvd_natCast] at h₂
    exact lt_iff_not_ge.mp h₀ <| Nat.le_of_dvd (Nat.sInf_mem (Set.nonempty_of_mem h₁)).1 h₂

theorem absNorm_under_dvd_absNorm {S : Type*} [CommRing S] [IsDedekindDomain S] [Module.Free ℤ S]
    (I : Ideal S) :
    absNorm (under ℤ I) ∣ absNorm I := by
  by_cases h : Finite (S ⧸ I)
  · have : Fintype (S ⧸ I) := Fintype.ofFinite (S ⧸ I)
    have h_main {d : ℕ} : (d : S) ∈ I ↔ ∀ (x : S ⧸ I), d • x = 0 := by
      simp_rw [nsmul_eq_mul, ← map_natCast (Ideal.Quotient.mk I), ← Quotient.eq_zero_iff_mem]
      exact ⟨fun h _ ↦ by simp [h], fun h ↦ by simpa using h 1⟩
    rw [Ideal.absNorm_apply I, Submodule.cardQuot_apply, Nat.card_eq_fintype_card]
    simp_rw [absNorm_under_eq_sInf, h_main, ← AddMonoid.exponent_eq_sInf]
    exact AddGroup.exponent_dvd_card (G := S ⧸ I)
  · rw [show absNorm I = 0 by
      exact AddSubgroup.index_eq_zero_iff_infinite.mpr <| not_finite_iff_infinite.mp h]
    exact Nat.dvd_zero _

end Int
